Inference at * 1 2 
Iof proof for Lemma eqff to assert:



1. ff = ff
  (ff) 

latex

 by BoolEval 

latex

 1: 

 1:   tt
 .

Definitions

if b then t else f fi , b, ff